$\forall$$T$:Type. $T$ $\subseteq\rho$ $\mathbb{Z}$ $\Rightarrow$ ($\forall$$x$:$T$, $L$:$T$ List, $z$:$T$. ($z$ $\in$ s{-}insert($x$;$L$)) $\Leftrightarrow$ $z$ $=$ $x$ $\vee$ ($z$ $\in$ $L$))